Model checking is a method of formal verification that is gaining in popularity as a tool for use in designing complex systems, such as integrated circuits. Model checking is typically carried out automatically by a symbolic model checking program, such as SMV. Model checking methods are described generally by Clarke et al. in Model Checking (MIT Press, 1999), which is incorporated herein by reference.
To perform model checking of the design of a device, a user reads the definition and functional specifications of the device and then, based on this information, writes a set of properties {φ} (also known as a specification) that the design is expected to fulfill. The properties are written in a suitable specification language for expressing temporal logic relationships between the inputs and outputs of the device. Such languages are commonly based on Computation Tree Logic (CTL) and/or Linear Time Logic (LTL). A hardware model M (also known as an implementation) of the design, which is typically written in a hardware description language, such as VHDL or Verilog, is then tested to ascertain that the model satisfies all of the properties in the set, i.e., that M I=φ, under all relevant input sequences.
Symbolic CTL model checking involves computing the transition-relation (TR) of the model, and then applying the model checking algorithm to verify a given formula. One of the most useful features of model checking is its ability, when a property φ is found to be false on M, to construct a sequence of states and transitions (known as a path, or trace) that leads to the problematic state of the design. This path is called a counterexample. It can be used by the engineer in understanding and remedying the design defect that led to the failure of the model. In many cases, however, the full TR is too big to be computed, or the model state space “explodes” before the model checker can find a counterexample or, in the alternative, verify the formula in question.
A number of solutions to this problem have been proposed, among them localization reduction, as described, for example, by Kurshan in Computer-Aided Verification of Coordinating Processes (Princeton University Press, 1994), pages 170-172, which is incorporated herein by reference. Localization reduction starts with an abstraction of the model under verification, i.e., with a model in which some of the variables are abstracted by eliminating them from the model or allowing them to take arbitrary values. As a result of this abstraction, the transition relation of the abstract model is more compact and easier to compute, but the behavior of the abstract model typically includes paths that do not exist in the complete model (also referred to as the concrete model). If a specification property is found to be true on the abstract model (i.e., no counterexample exists), then it is necessarily true on the complete model, as well, and no further verification of the property is needed.
When a counterexample is found on the abstract model, however, it is not certain that a counterexample exists in the complete model. To determine whether the abstract counterexample is valid, the model checker attempts to find an actual counterexample path on the complete model that corresponds to the abstract counterexample. This process is known as reconstruction of the abstract path. When the abstract path is successfully reconstructed, the counterexample is shown to be valid on the complete model, as well, and can be reported to the user as proof of failure of the property. When the abstract counterexample cannot be reconstructed on the complete model, it is considered to be spurious and is discarded. The abstract model may then be refined, typically by adding back in some of the variables that were previously abstracted, and the model checker continues to seek counterexamples on the refined abstract model. The process of reconstruction and refinement continues iteratively until the property is proven true or a valid counterexample is found.
The manner in which the abstract counterexample is reconstructed and, subsequently, the abstract model is refined following a failure of abstraction reduction is of key importance in making the localization reduction technique run efficiently. A number of authors have attempted to address the issue of abstraction reconstruction and refinement.
For example, Clarke et al. describe a method for automatic refinement of the abstract model using information obtained from erroneous counterexamples in “Counterexample-guided Abstraction Refinement,” in Proceedings of the Twelfth International Conference on Computer-Aided Verification (CAV 2000), pages 154-169, which is incorporated herein by reference. According to this method, as described by the authors, when a counterexample is found in the abstract model, all the corresponding concrete paths (i.e., actual paths) are computed in the complete model. When no concrete path can be found, the abstract counterexample is considered to be spurious. The model checker then finds the shortest prefix of the abstract counterexample that does not correspond to an actual trace in the full model. The last abstract state in this prefix is split into less abstract states in such a way that the spurious counterexample is eliminated from the abstract model. (Note that each abstract state in the abstract model corresponds to multiple states in the concrete model.) Thus, a more refined abstraction is obtained, which is then used in seeking and reconstructing new counterexamples.
Although Clarke et al. showed their counterexample-guided refinement method to work in some cases, the reconstruction of all concrete paths corresponding to a long abstract path in a complex system can itself result in state explosion. Furthermore, determining the optimal refinement at each iteration is a NP-hard problem, and Clarke et al. use an approximate refinement technique that is admittedly sub-optimal. There is therefore a need for more efficient automatic methods of symbolic localization reduction.